package autoz.czt.launching;

import java.util.List;

import net.sourceforge.czt.parser.util.CztError;
import net.sourceforge.czt.parser.util.ParseException;
import net.sourceforge.czt.session.CommandException;
import net.sourceforge.czt.session.Key;
import net.sourceforge.czt.session.SectionManager;
import net.sourceforge.czt.z.ast.Spec;
import autoz.core.problems.UmlProblem;
import autoz.czt.visitor.CZTUtils;
import autoz.czt.visitor.ErrorVisitor;

/**
 * 
 * @author jw
 *
 */
public class CZTEngine {

	private String filePath;
	
	SectionManager manager = new SectionManager();
	Spec spec;
	
	public CZTEngine(String filePath){
		this.filePath = filePath;
	}
	
	/**
	 * Use CZT to parse the document. 
	 * @return A list of parse errors.
	 * @throws CommandException
	 */
	public List<CztError> parse() throws CommandException{
		spec = CZTUtils.parseSpec(filePath, manager);	
		
		// Check for exceptions
		ParseException parseException = manager.get(new Key<ParseException>(filePath, ParseException.class));
		if (parseException != null){
			return parseException.getErrors();
		}
		
		return null;
	}
	
	/**
	 * Uses CZT to type check the specification.
	 * @return A list of errors associated directly with the UML diagram instead of the Z.
	 */
	public List<UmlProblem> typecheck(){
		CZTUtils.typecheck(spec, manager);
		
		ErrorVisitor v = new ErrorVisitor();
		spec.accept(v);
		
		return v.getErrors();
	}
}
